i:Id, A:Top. (@i: A(i)) ~ A 

latex

Definitions	Top, @i: A, Unit, P  Q, P & Q, a = b, , b, Id, t  T, Prop, b, x:A. B(x), A, P  Q, False
Lemmas	assert wf, not wf, Id wf, bnot wf, bool wf, eq id wf, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, top wf